Computational psychology has the aim to explain human cognition bycomputational models of cognitive processes. The cognitive architecture ACT-Ris popular to develop such models. Although ACT-R has a well-definedpsychological theory and has been used to explain many cognitive processes,there are two problems that make it hard to reason formally about its cognitivemodels: First, ACT-R lacks a formalization of its underlying production rulesystem and secondly, there are many different implementations and extensions ofACT-R with technical artifacts complicating formal reasoning even more. This paper describes a formal operational semantics - the very abstractsemantics - that abstracts from as many technical details as possible keepingit open to extensions and different implementations of the ACT-R theory. In asecond step, this semantics is refined to define some of its abstract featuresthat are found in many implementations of ACT-R - the abstract semantics. Itconcentrates on the procedural core of ACT-R and is suitable for analysis ofthe transition system since it still abstracts from details like timing, thesub-symbolic layer or conflict resolution. Furthermore, a translation of ACT-R models to the programming languageConstraint Handling Rules (CHR) is defined. This makes the abstract semanticsan executable specification of ACT-R. CHR has been used successfully to embedother rule-based formalisms like graph transformation systems or functionalprogramming. There are many results and tools that support formal reasoningabout and analysis of CHR programs. The translation of ACT-R models to CHR isproven sound and complete w.r.t. the abstract operational semantics of ACT-R.This paves the way to analysis of ACT-R models through CHR. Therefore, to thebest of our knowledge, our abstract semantics is the first formulation of ACT-Rsuitable for both analysis and execution.
展开▼
